1 /-
2 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Robert Y. Lewis
5 -/
6
7 import data.padics.padic_integers data.polynomial topology.metric_space.cau_seq_filter
src └────────────────────────┘ └─────────────┘ └──────────────────────────────────┘
8 import analysis.specific_limits topology.algebra.polynomial
src └──────────────────────┘ └─────────────────────────┘
9
10 /-!
11 # Hensel's lemma on ℤ_p
12
13 This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:
14 <http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf>
15
16 Hensel's lemma gives a simple condition for the existence of a root of a polynomial.
17
18 The proof and motivation are described in the paper
19 [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019].
20
21 ## References
22
23 * <http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf>
24 * [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
25 * <https://en.wikipedia.org/wiki/Hensel%27s_lemma>
26
27 ## Tags
28
29 p-adic, p adic, padic, p-adic integer
30 -/
31
32 noncomputable theory
33
34 open_locale classical topological_space
35
36 -- We begin with some general lemmas that are used below in the computation.
37
38 lemma padic_polynomial_dist {p : ℕ} [p.prime] (F : polynomial ℤ_[p]) (x y : ℤ_[p]) :
id ┴ ┴└────┘ └────────┘ └─┘┴┴ └─┘┴┴
src ┴ └────┘ └────────┘ └─┘ ┴ └─┘ ┴
typ ┴ ┴└────┘ └────────┘ └─┘┴┴ └─┘┴┴
doc └────┘ └────────┘ └─┘ ┴ └─┘ ┴
39 ∥F.eval x - F.eval y∥ ≤ ∥x - y∥ :=
id ┴┴└───┘ ┴ ┴ ┴└───┘ ┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴┴└───┘ ┴ ┴ ┴└───┘ ┴┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ └───┘
40 let ⟨z, hz⟩ := F.eval_sub_factor x y in calc
41 ∥F.eval x - F.eval y∥ = ∥z∥ * ∥x - y∥ : by simp [hz]
src └────┘ └─
typ └────┘ └─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
42 ... ≤ 1 * ∥x - y∥ : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id └────────────────────────┘ └─────────────────┘ └─────────┘
src ───┘ └────────────────────────┘ └─────────────────┘ └─────────┘
typ ───┘ └────────────────────────┘ └─────────────────┘ └─────────┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
43 ... = ∥x - y∥ : by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
44
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
45 open filter metric
46
47 private lemma comp_tendsto_lim {p : ℕ} [p.prime] {F : polynomial ℤ_[p]} (ncs : cau_seq ℤ_[p] norm) :
id └┘┴┴ └──┘
src └┘ ┴ └──┘
typ └┘┴┴ └──┘
doc └┘ ┴
48 tendsto (λ i, F.eval (ncs i)) at_top (𝓝 (F.eval ncs.lim)) :=
id └─────┘ ┴ ┴└───┘ └─┘ ┴ └────┘ ┴ ┴└───┘ └─┘└──┘
src └─────┘ └───┘ └────┘ ┴ └───┘ └──┘
typ └─────┘ ┴ ┴└───┘ └─┘ ┴ └────┘ ┴ ┴└───┘ └─┘└──┘
doc └─────┘ └───┘ └────┘ ┴ └───┘
49 (F.continuous_eval.tendsto _).comp ncs.tendsto_limit
50
51 section
52 parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]} {a : ℤ_[p]}
53 (ncs_der_val : ∀ n, ∥F.derivative.eval (ncs n)∥ = ∥F.derivative.eval a∥)
54 include ncs_der_val
55
56 private lemma ncs_tendsto_const :
57 tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (𝓝 ∥F.derivative.eval a∥) :=
id └┘ ┴ ┴ └────┘ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └────┘ ┴ ┴ └─────────┘└───┘ ┴
typ └┘ ┴ ┴ └────┘ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └────┘ ┴ └─────────┘└───┘
58 by convert tendsto_const_nhds; ext; rw ncs_der_val
id └──┘ └─────────┘
src └──────┘ └──┘ └─┘ └─┘ └
typ └──────┘ └──┘ └─┘ └─┘└─────────┘└
doc └──────┘ └─┘ └─┘ └
txt └──────┘ └─┘ └─┘ └
par └──────┘ └─┘ └─┘ └
pid ┴ ┴ └
st └────────────┘└─────────┘└
59
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
60 private lemma ncs_tendsto_lim :
61 tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (𝓝 (∥F.derivative.eval ncs.lim∥)) :=
id └─────┘ ┴ ┴┴└─────────┘└───┘ └─┘ ┴ ┴ └────┘ ┴ ┴┴└─────────┘└───┘ └─┘└──┘┴
src └─────┘ ┴ └─────────┘└───┘ ┴ └────┘ ┴ ┴ └─────────┘└───┘ └──┘┴
typ └─────┘ ┴ ┴┴└─────────┘└───┘ └─┘ ┴ ┴ └────┘ ┴ ┴┴└─────────┘└───┘ └─┘└──┘┴
doc └─────┘ └─────────┘└───┘ └────┘ ┴ └─────────┘└───┘
62 tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _) (comp_tendsto_lim _)
id └──────────┘ └──────────────────────────┘┴ └─────────────┘ └──────────────┘
src └──────────┘ └──────────────────────────┘┴ └─────────────┘ └──────────────┘
typ └──────────┘ └──────────────────────────┘┴ └─────────────┘ └──────────────┘
63
64 private lemma norm_deriv_eq : ∥F.derivative.eval ncs.lim∥ = ∥F.derivative.eval a∥ :=
id ┴┴└─────────┘└───┘ └─┘└──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ └──┘┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └─┘└──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘
65 tendsto_nhds_unique at_top_ne_bot ncs_tendsto_lim ncs_tendsto_const
id └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
src └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
typ └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
66
67 end
68
69 section
70 parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]}
id ┴ └───────┘ └─────┘ └─┘ ┴ └──┘ └────────┘ └─┘ ┴
src ┴ └───────┘ └─────┘ └─┘ ┴ └──┘ └────────┘ └─┘ ┴
typ ┴ └───────┘ └─────┘ └─┘ ┴ └──┘ └────────┘ └─┘ ┴
doc └───────┘ └─┘ ┴ └────────┘ └─┘ ┴
71 (hnorm : tendsto (λ i, ∥F.eval (ncs i)∥) at_top (𝓝 0))
id └─────┘ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴
src └─────┘ ┴ └───┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴
doc └─────┘ └───┘ └────┘ ┴
72 include hnorm
73
74 private lemma tendsto_zero_of_norm_tendsto_zero : tendsto (λ i, F.eval (ncs i)) at_top (𝓝 0) :=
id └─────┘ ┴ ┴└───┘ └─┘ ┴ └────┘ ┴
src └─────┘ └───┘ └────┘ ┴
typ └─────┘ ┴ ┴└───┘ └─┘ ┴ └────┘ ┴
doc └─────┘ └───┘ └────┘ ┴
75 tendsto_iff_norm_tendsto_zero.2 (by simpa using hnorm)
id └───────────────────────────┘┴ └───┘
src └───────────────────────────┘┴ └──────────┘
typ └───────────────────────────┘┴ └──────────┘└───┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────────┘
76
77 lemma limit_zero_of_norm_tendsto_zero : F.eval ncs.lim = 0 :=
id ┴└───┘ └─┘└──┘ ┴
src └───┘ └──┘ ┴
typ ┴└───┘ └─┘└──┘ ┴
doc └───┘
78 tendsto_nhds_unique at_top_ne_bot (comp_tendsto_lim _) tendsto_zero_of_norm_tendsto_zero
id └─────────────────┘ └───────────┘ └──────────────┘ └───────────────────────────────┘
src └─────────────────┘ └───────────┘ └──────────────┘ └───────────────────────────────┘
typ └─────────────────┘ └───────────┘ └──────────────┘ └───────────────────────────────┘
79
80 end
81
82 section hensel
83 open nat
84
85 parameters {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
id ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
src ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
typ ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
doc └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
86 (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2) (hnsol : F.eval a ≠ 0)
id ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ └───┘ ┴
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ └───┘ ┴
doc └───┘ └─────────┘└───┘ └───┘
87 include hnorm
88
89 /-- `T` is an auxiliary value that is used to control the behavior of the polynomial `F`. -/
90 private def T : ℝ := ∥(F.eval a).val / ((F.derivative.eval a).val)^2∥
id ┴ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└─────────┘└───┘ ┴ └─┘ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴ └─────────┘└───┘ └─┘ ┴ ┴
typ ┴ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└─────────┘└───┘ ┴ └─┘ ┴ ┴
doc └───┘ └─────────┘└───┘
91
92 private lemma deriv_sq_norm_pos : 0 < ∥F.derivative.eval a∥ ^ 2 :=
id ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
src ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
doc └─────────┘└───┘
93 lt_of_le_of_lt (norm_nonneg _) hnorm
id └────────────┘ └─────────┘ └───┘
src └────────────┘ └─────────┘
typ └────────────┘ └─────────┘ └───┘
94
95 private lemma deriv_sq_norm_ne_zero : ∥F.derivative.eval a∥^2 ≠ 0 := ne_of_gt deriv_sq_norm_pos
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ └──────┘ └───────────────┘
src ┴ └─────────┘└───┘ ┴┴ ┴ └──────┘ └───────────────┘
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ └──────┘ └───────────────┘
doc └─────────┘└───┘
96
97 private lemma deriv_norm_ne_zero : ∥F.derivative.eval a∥ ≠ 0 :=
id ┴┴└─────────┘└───┘ ┴┴ ┴
src ┴ └─────────┘└───┘ ┴ ┴
typ ┴┴└─────────┘└───┘ ┴┴ ┴
doc └─────────┘└───┘
98 λ h, deriv_sq_norm_ne_zero (by simp [*, _root_.pow_two])
id ┴ └───────────────────┘ └────────────┘
src └───────────────────┘ └───────┘└────────────┘┴
typ ┴ └───────────────────┘ └───────┘└────────────┘┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└──┘ ┴
st └───────────────────────┘
99
100 private lemma deriv_norm_pos : 0 < ∥F.derivative.eval a∥ :=
id ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ ┴ └─────────┘└───┘ ┴
typ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘
101 lt_of_le_of_ne (norm_nonneg _) (ne.symm deriv_norm_ne_zero)
id └────────────┘ └─────────┘ └─────┘ └────────────────┘
src └────────────┘ └─────────┘ └─────┘ └────────────────┘
typ └────────────┘ └─────────┘ └─────┘ └────────────────┘
102
103 private lemma deriv_ne_zero : F.derivative.eval a ≠ 0 := mt (norm_eq_zero _).2 deriv_norm_ne_zero
id ┴└─────────┘└───┘ ┴ ┴ └┘ └──────────┘ ┴ └────────────────┘
src └─────────┘└───┘ ┴ └┘ └──────────┘ ┴ └────────────────┘
typ ┴└─────────┘└───┘ ┴ ┴ └┘ └──────────┘ ┴ └────────────────┘
doc └─────────┘└───┘
104
105 private lemma T_def : T = ∥F.eval a∥ / ∥F.derivative.eval a∥^2 :=
id ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
src ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴
typ ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
doc ┴ └───┘ └─────────┘└───┘
106 calc T = ∥(F.eval a).val∥ / ∥((F.derivative.eval a).val)^2∥ : normed_field.norm_div _ _
id ┴ ┴ ┴└───┘ ┴ └─┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘ ┴ ┴ └───────────────────┘
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ └─┘ ┴ ┴ └───────────────────┘
typ ┴ ┴ ┴└───┘ ┴ └─┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘ ┴ ┴ └───────────────────┘
doc ┴ └───┘ └─────────┘└───┘
107 ... = ∥F.eval a∥ / ∥(F.derivative.eval a)^2∥ : by simp [norm, padic_norm_z]
id ┴┴└───┘ ┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └──────────┘
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ └────┘ └┘└──────────┘└─
typ ┴┴└───┘ ┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └────┘ └┘└──────────┘└─
doc └───┘ └─────────┘└───┘ └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────
108 ... = ∥F.eval a∥ / ∥(F.derivative.eval a)∥^2 : by simp [pow, monoid.pow]
id ┴┴└───┘ ┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴┴ └────────┘
src ──┘ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ └────┘ └┘└────────┘└─
typ ──┘ ┴┴└───┘ ┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴┴ └────┘ └┘└────────┘└─
doc ──┘ └───┘ └─────────┘└───┘ └────┘ └┘└────────┘└─
txt ──┘ └────┘ └┘ └─
par ──┘ └────┘ └┘ └─
pid ──┘ ┴┴ └┘ ┴└
st ──┘ └───────────────────────
109
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
110 private lemma T_lt_one : T < 1 :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
111 let h := (div_lt_one_iff_lt deriv_sq_norm_pos).2 hnorm in
id ┴ └───────────────┘ └───────────────┘ ┴ └───┘
src └───────────────┘ └───────────────┘ ┴
typ ┴ └───────────────┘ └───────────────┘ ┴ └───┘
112 by rw T_def; apply h
id └───┘
src └─┘└───┘ └────┘ └
typ └─┘└───┘ └────┘ └
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └──────────────────
113
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
114 private lemma T_pow {n : ℕ} (hn : n > 0) : T ^ n < 1 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
115 have T ^ n ≤ T ^ 1, from pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) (succ_le_of_lt hn),
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └───────────┘ └┘
src ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └───────────┘ └┘
doc ┴ ┴
116 lt_of_le_of_lt (by simpa) T_lt_one
id └────────────┘ └──────┘
src └────────────┘ └───┘ └──────┘
typ └────────────┘ └───┘ └──────┘
doc └───┘
txt └───┘
par └───┘
st └────┘
117
118 private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := (T_pow (nat.pow_pos (by norm_num) _))
id ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─────────┘
src ┴ ┴ ┴ ┴ ┴ └───┘ └─────────┘ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─────────┘ └──────┘
doc ┴ └──────┘
txt └──────┘
par └──────┘
st └───────┘
119
120 private lemma T_pow_nonneg (n : ℕ) : T ^ n ≥ 0 := pow_nonneg (norm_nonneg _) _
id ┴ ┴ ┴ ┴ ┴ └────────┘ └─────────┘
src ┴ ┴ ┴ ┴ └────────┘ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────┘ └─────────┘
doc ┴
121
122 /-- We will construct a sequence of elements of ℤ_p satisfying successive values of `ih`. -/
123 private def ih (n : ℕ) (z : ℤ_[p]) : Prop :=
id ┴ └─┘┴┴
src ┴ └─┘ ┴
typ ┴ └─┘┴┴
doc └─┘ ┴
124 ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧ ∥F.eval z∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n)
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴
src ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ ┴ ┴ ┴ ┴
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘ └───┘ └─────────┘└───┘ ┴
125
126 private lemma ih_0 : ih 0 a :=
id └┘ ┴
src └┘
typ └┘ ┴
doc └┘
127 ⟨ rfl, by simp [T_def, mul_div_cancel' _ (ne_of_gt (deriv_sq_norm_pos hnorm))] ⟩
id └─┘ └───┘ └─────────────┘ └──────┘ └───────────────┘ └───┘
src └─┘ └────┘└───┘└┘└─────────────┘└─┘ └──────┘┴ └───────────────┘┴ └──┘
typ └─┘ └────┘└───┘└┘└─────────────┘└─┘ └──────┘┴ └───────────────┘┴└───┘└──┘
doc └────┘ └┘ └─┘ ┴ ┴ └──┘
txt └────┘ └┘ └─┘ ┴ ┴ └──┘
par └────┘ └┘ └─┘ ┴ ┴ └──┘
pid ┴┴ └┘ └─┘ ┴ ┴ └─┘┴
st └────────────────────────────────────────────────────────────────────┘
128
129 private lemma calc_norm_le_one {n : ℕ} {z : ℤ_[p]} (hz : ih n z) :
id ┴ └─┘┴┴ └┘ ┴ ┴
src ┴ └─┘ ┴ └┘
typ ┴ └─┘┴┴ └┘ ┴ ┴
doc └─┘ ┴ └┘
130 ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1 :=
id ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴
doc └───┘ └─┘ ┴ └─────────┘└───┘
131 calc ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥
id ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴
doc └───┘ └─┘ ┴ └─────────┘└───┘
132 = ∥(↑(F.eval z) : ℚ_[p])∥ / ∥(↑(F.derivative.eval z) : ℚ_[p])∥ : normed_field.norm_div _ _
id ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴ └───────────────────┘
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ └─┘ ┴ ┴ └───────────────────┘
typ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴ └───────────────────┘
doc └───┘ └─┘ ┴ └─────────┘└───┘ └─┘ ┴
133 ... = ∥F.eval z∥ / ∥F.derivative.eval a∥ : by simp [hz.1]
id ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ └────┘ └──┘
typ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └────┘└┘└──┘
doc └───┘ └─────────┘└───┘ └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴┴ └─┘┴
st └───────────┘
134 ... ≤ ∥F.derivative.eval a∥^2 * T^(2^n) / ∥F.derivative.eval a∥ :
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ ┴ └─────────┘└───┘
135 (div_le_div_right deriv_norm_pos).2 hz.2
id └──────────────┘ └────────────┘ ┴ └┘┴
src └──────────────┘ └────────────┘ ┴ ┴
typ └──────────────┘ └────────────┘ ┴ └┘┴
136 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel (ne_of_gt deriv_norm_pos) _
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └──────┘ └────────────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ └───────────┘ └──────┘ └────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └──────┘ └────────────┘
doc └─────────┘└───┘ ┴
137 ... ≤ 1 : mul_le_one (padic_norm_z.le_one _) (T_pow_nonneg _) (le_of_lt (T_pow' _))
id └────────┘ └─────────────────┘ └──────────┘ └──────┘ └────┘
src └────────┘ └─────────────────┘ └──────────┘ └──────┘ └────┘
typ └────────┘ └─────────────────┘ └──────────┘ └──────┘ └────┘
138
139 private lemma calc_deriv_dist {z z' z1 : ℤ_[p]} (hz' : z' = z - z1)
id └─┘┴┴ └┘ ┴ ┴ ┴ └┘
src └─┘ ┴ ┴ ┴
typ └─┘┴┴ └┘ ┴ ┴ ┴ └┘
doc └─┘ ┴
140 (hz1 : ∥z1∥ = ∥F.eval z∥ / ∥F.derivative.eval a∥) {n} (hz : ih n z) :
id ┴└┘┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ └┘
typ ┴└┘┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
doc └───┘ └─────────┘└───┘ └┘
141 ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥ :=
id ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘ └─────────┘└───┘
142 calc
143 ∥F.derivative.eval z' - F.derivative.eval z∥
id ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘
144 ≤ ∥z' - z∥ : padic_polynomial_dist _ _ _
id ┴└┘ ┴ ┴┴ └───────────────────┘
src ┴ ┴ ┴ └───────────────────┘
typ ┴└┘ ┴ ┴┴ └───────────────────┘
145 ... = ∥z1∥ : by simp [hz']
id ┴└┘┴ └─┘
src ┴ ┴ └────┘ └┘
typ ┴└┘┴ └────┘└─┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────┘
146 ... = ∥F.eval z∥ / ∥F.derivative.eval a∥ : hz1
id ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └─┘
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └─┘
doc └───┘ └─────────┘└───┘
147 ... ≤ ∥F.derivative.eval a∥^2 * T^(2^n) / ∥F.derivative.eval a∥ : (div_le_div_right deriv_norm_pos).2 hz.2
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └──────────────┘ └────────────┘ ┴ └┘┴
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ └──────────────┘ └────────────┘ ┴ ┴
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └──────────────┘ └────────────┘ ┴ └┘┴
doc └─────────┘└───┘ ┴ └─────────┘└───┘
148 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel deriv_norm_ne_zero _
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └────────────────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ └───────────┘ └────────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └────────────────┘
doc └─────────┘└───┘ ┴
149 ... < ∥F.derivative.eval a∥ : (mul_lt_iff_lt_one_right deriv_norm_pos).2 (T_pow (pow_pos (by norm_num) _))
id ┴┴└─────────┘└───┘ ┴┴ └─────────────────────┘ └────────────┘ ┴ └───┘ └─────┘
src ┴ └─────────┘└───┘ ┴ └─────────────────────┘ └────────────┘ ┴ └───┘ └─────┘ └──────┘
typ ┴┴└─────────┘└───┘ ┴┴ └─────────────────────┘ └────────────┘ ┴ └───┘ └─────┘ └──────┘
doc └─────────┘└───┘ └──────┘
txt └──────┘
par └──────┘
st └───────┘
150
151 private def calc_eval_z' {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n z)
id └─┘┴┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └┘
typ └─┘┴┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴
doc └─┘ ┴ └┘
152 (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
id ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └┘ ┴ └┘
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴
typ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └┘ ┴ └┘
doc └───┘ └─┘ ┴ └─────────┘└───┘
153 {q : ℤ_[p] // F.eval z' = q * z1^2} :=
id ┴ └─┘┴┴ ┴└───┘ └┘ ┴ ┴ ┴ └┘┴
src ┴ └─┘ ┴ └───┘ ┴ ┴ ┴
typ ┴ └─┘┴┴ ┴└───┘ └┘ ┴ ┴ ┴ └┘┴
doc └─┘ ┴ └───┘
154 have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0, from
id ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴
src ┴ └─────────┘└───┘ └─┘ ┴ ┴
typ ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴
doc └─────────┘└───┘ └─┘ ┴
155 have hdzne : F.derivative.eval z ≠ 0,
id ┴└─────────┘└───┘ ┴ ┴
src └─────────┘└───┘ ┴
typ ┴└─────────┘└───┘ ┴ ┴
doc └─────────┘└───┘
156 from mt (norm_eq_zero _).2 (by rw hz.1; apply deriv_norm_ne_zero; assumption),
id └┘ └──────────┘ ┴ └┘ └────────────────┘
src └┘ └──────────┘ ┴ └─┘ └┘ └────┘└────────────────┘ └────────┘
typ └┘ └──────────┘ ┴ └─┘└┘└┘ └────┘└────────────────┘ └────────┘
doc └─┘ └┘ └────┘ └────────┘
txt └─┘ └┘ └────┘ └────────┘
par └─┘ └┘ └────┘ └────────┘
pid ┴ └┘ ┴
st └────────────────────────────────────────────┘
157 λ h, hdzne $ subtype.ext.2 h,
id ┴ └───┘ └─────────┘┴ ┴
src └─────────┘┴
typ ┴ └───┘ └─────────┘┴ ┴
158 let ⟨q, hq⟩ := F.binom_expansion z (-z1) in
id └─┘ ┴ ┴└──────────────┘ ┴ ┴└┘
src └──────────────┘ ┴
typ └─┘ ┴ ┴└──────────────┘ ┴ ┴└┘
159 have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])∥ ≤ 1,
id ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴ ┴
src ┴ ┴ └─────────┘└───┘ ┴ ┴ └───┘ ┴ ┴ └─────────┘└───┘ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └─┘┴┴ ┴ ┴
doc └─────────┘└───┘ └───┘ └─────────┘└───┘ └─┘ ┴
160 by {rw padic_norm_e.mul, apply mul_le_one, apply padic_norm_z.le_one, apply norm_nonneg, apply h1},
id └──────────────┘ └────────┘ └─────────────────┘ └─────────┘
src └─┘└──────────────┘ └────┘└────────┘ └────┘└─────────────────┘ └────┘└─────────┘ └────┘
typ └─┘└──────────────┘ └────┘└────────┘ └────┘└─────────────────┘ └────┘└─────────┘ └────┘
doc └─┘ └────┘ └────┘ └────┘ └────┘
txt └─┘ └────┘ └────┘ └────┘ └────┘
par └─┘ └────┘ └────┘ └────┘ └────┘
pid ┴ ┴ ┴ ┴ ┴
st └───────────────────┘└────────────────┘└─────────────────────────┘└─────────────────┘└────────┘└┘
161 have F.derivative.eval z * (-z1) = -F.eval z, from calc
id ┴└─────────┘└───┘ ┴ ┴ ┴└┘ ┴ ┴┴└───┘ ┴
src └─────────┘└───┘ ┴ ┴ ┴ ┴ └───┘
typ ┴└─────────┘└───┘ ┴ ┴ ┴└┘ ┴ ┴┴└───┘ ┴
doc └─────────┘└───┘ └───┘
162 F.derivative.eval z * (-z1)
id ┴└─────────┘└───┘ ┴ ┴ ┴└┘
src └─────────┘└───┘ ┴ ┴
typ ┴└─────────┘└───┘ ┴ ┴ ┴└┘
doc └─────────┘└───┘
163 = (F.derivative.eval z) * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ : by rw [hzeq]
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └┘ └──┘
src └─────────┘└───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─────────┘└───┘ └──┘ └┘
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └┘ └──┘└──┘└┘
doc └─────────┘└───┘ └───┘ └─────────┘└───┘ └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st └───────┘┴┴
164 ... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp
id ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └┘
src ┴ └─────────┘└───┘ ┴ ┴ └───┘ ┴ ┴ └─────────┘└───┘ └───┘
typ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └┘ └───┘
doc └─────────┘└───┘ └───┘ └─────────┘└───┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
165 ... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext.2 $ by simp
id ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └──┘ └─────────┘┴
src ┴ ┴ └─────────┘└───┘ ┴ ┴ └───┘ ┴ ┴ └─────────┘└───┘ └─────────┘┴ └───┘
typ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴└─────────┘└───┘ ┴ └──┘ └─────────┘┴ └───┘
doc └─────────┘└───┘ └───┘ └─────────┘└───┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
166 ... = -(F.eval z) : by simp [mul_div_cancel' _ hdzne'],
id ┴ ┴└───┘ ┴ └─────────────┘ └────┘
src ┴ └───┘ └────┘└─────────────┘└─┘ ┴
typ ┴ ┴└───┘ ┴ └────┘└─────────────┘└─┘└────┘┴
doc └───┘ └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴┴ └─┘ ┴
st └──────────────────────────────┘
167 have heq : F.eval z' = q * z1^2, by simpa [this, hz'] using hq,
id ┴└───┘ └┘ ┴ ┴ └┘┴ └──┘ └─┘ └┘
src └───┘ ┴ ┴ ┴ └─────┘ └┘ └──────┘
typ ┴└───┘ └┘ ┴ ┴ └┘┴ └─────┘└──┘└┘└─┘└──────┘└┘
doc └───┘ └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └─────────────────────────┘
168 ⟨q, heq⟩
id └─┘
src └─┘
typ └─┘
169
170 private def calc_eval_z'_norm {z z' z1 : ℤ_[p]} {n} (hz : ih n z) {q}
id └─┘┴┴ └┘ ┴ ┴
src └─┘ ┴ └┘
typ └─┘┴┴ └┘ ┴ ┴
doc └─┘ ┴ └┘
171 (heq : F.eval z' = q * z1^2) (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1)
id ┴└───┘ └┘ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴└───┘ └┘ ┴ ┴ ┴ └┘┴ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴
doc └───┘ └───┘ └─┘ ┴ └─────────┘└───┘
172 (hzeq : z1 = ⟨_, h1⟩) : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)) :=
id └┘ ┴ └┘ ┴┴└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴
typ └┘ ┴ └┘ ┴┴└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ └─────────┘└───┘ ┴
173 calc ∥F.eval z'∥
id ┴┴└───┘ └┘┴
src ┴ └───┘ ┴
typ ┴┴└───┘ └┘┴
doc └───┘
174 = ∥q∥ * ∥z1∥^2 : by simp [heq]
id ┴┴┴ ┴ ┴└┘┴┴ └─┘
src ┴ ┴ ┴ ┴ ┴┴ └────┘└─┘└┘
typ ┴┴┴ ┴ ┴└┘┴┴ └────┘└─┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────┘
175 ... ≤ 1 * ∥z1∥^2 : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (pow_nonneg (norm_nonneg _) _)
id ┴ ┴└┘┴┴ └────────────────────────┘ └─────────────────┘ └────────┘ └─────────┘
src ┴ ┴ ┴┴ └────────────────────────┘ └─────────────────┘ └────────┘ └─────────┘
typ ┴ ┴└┘┴┴ └────────────────────────┘ └─────────────────┘ └────────┘ └─────────┘
176 ... = ∥F.eval z∥^2 / ∥F.derivative.eval a∥^2 :
id ┴┴└───┘ ┴┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
src ┴ └───┘ ┴┴ ┴ ┴ └─────────┘└───┘ ┴┴
typ ┴┴└───┘ ┴┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
doc └───┘ └─────────┘└───┘
177 by simp [hzeq, hz.1, div_pow _ (deriv_norm_ne_zero hnorm)]
id └──┘ └┘ └─────┘ └────────────────┘ └───┘
src └────┘ └┘ └──┘└─────┘└─┘ └────────────────┘┴ └─┘
typ └────┘└──┘└┘└┘└──┘└─────┘└─┘ └────────────────┘┴└───┘└─┘
doc └────┘ └┘ └──┘ └─┘ ┴ └─┘
txt └────┘ └┘ └──┘ └─┘ ┴ └─┘
par └────┘ └┘ └──┘ └─┘ ┴ └─┘
pid ┴┴ └┘ └──┘ └─┘ ┴ └┘┴
st └───────────────────────────────────────────────────────┘
178 ... ≤ (∥F.derivative.eval a∥^2 * T^(2^n))^2 / ∥F.derivative.eval a∥^2 :
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴┴
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴
doc └─────────┘└───┘ ┴ └─────────┘└───┘
179 (div_le_div_right deriv_sq_norm_pos).2 (pow_le_pow_of_le_left (norm_nonneg _) hz.2 _)
id └──────────────┘ └───────────────┘ ┴ └───────────────────┘ └─────────┘ └┘┴
src └──────────────┘ └───────────────┘ ┴ └───────────────────┘ └─────────┘ ┴
typ └──────────────┘ └───────────────┘ ┴ └───────────────────┘ └─────────┘ └┘┴
180 ... = (∥F.derivative.eval a∥^2)^2 * (T^(2^n))^2 / ∥F.derivative.eval a∥^2 : by simp only [_root_.mul_pow]
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ └────────────┘
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ └─────────┘└────────────┘└┘
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ └─────────┘└────────────┘└┘
doc └─────────┘└───┘ ┴ └─────────┘└───┘ └─────────┘ └┘
txt └─────────┘ └┘
par └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st └──────────────────────────┘
181 ... = ∥F.derivative.eval a∥^2 * (T^(2^n))^2 : div_sq_cancel deriv_sq_norm_ne_zero _
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └───────────┘ └───────────────────┘
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ └───────────┘ └───────────────────┘
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └───────────┘ └───────────────────┘
doc └─────────┘└───┘ ┴
182 ... = ∥F.derivative.eval a∥^2 * T^(2^(n + 1)) : by rw [←pow_mul]; refl
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ └───┘└─────┘┴ └────
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴ ┴ └───┘└─────┘┴ └────
doc └─────────┘└───┘ ┴ └───┘ ┴ └────
txt └───┘ ┴ └────
par └───┘ ┴ └────
pid └─┘ ┴ └
st └───────────┘┴└──────
183
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
184 set_option eqn_compiler.zeta true
doc └───────────────┘
185
186 /-- Given `z : ℤ_[p]` satisfying `ih n z`, construct `z' : ℤ_[p]` satisfying `ih (n+1) z'`. We need
187 the hypothesis `ih n z`, since otherwise `z'` is not necessarily an integer. -/
188 private def ih_n {n : ℕ} {z : ℤ_[p]} (hz : ih n z) : {z' : ℤ_[p] // ih (n+1) z'} :=
id ┴ └─┘┴┴ └┘ ┴ ┴ ┴ └─┘┴┴ └┘ ┴┴ └┘
src ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ └┘ ┴
typ ┴ └─┘┴┴ └┘ ┴ ┴ ┴ └─┘┴┴ └┘ ┴┴ └┘
doc └─┘ ┴ └┘ └─┘ ┴ └┘
189 have h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1, from calc_norm_le_one hz,
id ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └──────────────┘ └┘
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ └──────────────┘
typ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ ┴ ┴ ┴└─────────┘└───┘ ┴ ┴ ┴ └──────────────┘ └┘
doc └───┘ └─┘ ┴ └─────────┘└───┘
190 let z1 : ℤ_[p] := ⟨_, h1⟩,
id └─┘┴┴ └┘
src └─┘ ┴
typ └─┘┴┴ └┘
doc └─┘ ┴
191 z' : ℤ_[p] := z - z1 in
id └─┘┴┴ ┴ ┴ └┘
src └─┘ ┴ ┴
typ └─┘┴┴ ┴ ┴ └┘
doc └─┘ ┴
192 ⟨ z',
id └┘
typ └┘
193 have hdist : ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥,
id ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └┘ ┴ ┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘ └─────────┘└───┘
194 from calc_deriv_dist rfl (by simp [z1, hz.1]) hz,
id └─────────────┘ └─┘ └┘ └┘ └┘
src └─────────────┘ └─┘ └────┘ └┘ └─┘
typ └─────────────┘ └─┘ └────┘└┘└┘└┘└─┘ └┘
doc └────┘ └┘ └─┘
txt └────┘ └┘ └─┘
par └────┘ └┘ └─┘
pid ┴┴ └┘ └─┘
st └──────────────┘
195 have hfeq : ∥F.derivative.eval z'∥ = ∥F.derivative.eval a∥,
id ┴┴└─────────┘└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘
196 begin
st └─────
197 rw [sub_eq_add_neg, ← hz.1, ←norm_neg (F.derivative.eval z)] at hdist,
id └────────────┘ └┘ └──────┘ └───────────────┘ ┴
src └──┘└────────────┘└──┘ └───┘└──────┘┴ └───────────────┘┴ └─────────┘
typ └──┘└────────────┘└──┘└┘└───┘└──────┘┴ └───────────────┘┴┴└─────────┘
doc └──┘ └──┘ └───┘ ┴ └───────────────┘┴ └─────────┘
txt └──┘ └──┘ └───┘ ┴ ┴ └─────────┘
par └──┘ └──┘ └───┘ ┴ ┴ └─────────┘
pid └┘ └──┘ └───┘ ┴ ┴ └┘└───────┘
st ───────────────────────┘└────┘└─────────────────────────────────┘┴└───────┘└─
198 have := padic_norm_z.eq_of_norm_add_lt_right hdist,
id └──────────────────────────────────┘ └───┘
src └──────┘└──────────────────────────────────┘┴
typ └──────┘└──────────────────────────────────┘┴└───┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ───────────────────────────────────────────────────────┘└─
199 rwa [norm_neg, hz.1] at this
id └──────┘ └┘
src └───┘└──────┘└┘ └───────────
typ └───┘└──────┘└┘└┘└───────────
doc └───┘ └┘ └───────────
txt └───┘ └┘ └───────────
par └───┘ └┘ └───────────
pid └┘ └┘ └─┘└──────┘└
st ──────────────────┘└──┘└─┘└────────
200 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
201 let ⟨q, heq⟩ := calc_eval_z' rfl hz h1 rfl in
id └─┘ └─┘ └──────────┘ └─┘ └┘ └┘ └─┘
src └─┘ └──────────┘ └─┘ └─┘
typ └─┘ └─┘ └──────────┘ └─┘ └┘ └┘ └─┘
202 have hnle : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)),
id ┴┴└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴
typ ┴┴└───┘ └┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ └─────────┘└───┘ ┴
203 from calc_eval_z'_norm hz heq h1 rfl,
id └───────────────┘ └┘ └┘ └─┘
src └───────────────┘ └─┘
typ └───────────────┘ └┘ └┘ └─┘
204 ⟨hfeq, hnle⟩⟩
id └──┘ └──┘
typ └──┘ └──┘
205
206 set_option eqn_compiler.zeta false
doc └───────────────┘
207
208 -- why doesn't "noncomputable theory" stick here?
209 private noncomputable def newton_seq_aux : Π n : ℕ, {z : ℤ_[p] // ih n z}
id ┴ ┴ ┴ └─┘┴┴ └┘ ┴ ┴
src ┴ ┴ └─┘ ┴ └┘
typ ┴ ┴ ┴ └─┘┴┴ └┘ ┴ ┴
doc └─┘ ┴ └┘
210 | 0 := ⟨a, ih_0⟩
id ┴ └──┘
src └──┘
typ ┴ └──┘
211 | (k+1) := ih_n (newton_seq_aux k).2
id ┴┴ └──┘ └────────────┘ ┴
src ┴ └──┘ ┴
typ ┴┴ └──┘ └────────────┘ ┴
doc └──┘
212
213 private def newton_seq (n : ℕ) : ℤ_[p] := (newton_seq_aux n).1
id ┴ └─┘┴┴ └────────────┘ ┴ ┴
src ┴ └─┘ ┴ └────────────┘ ┴
typ ┴ └─┘┴┴ └────────────┘ ┴ ┴
doc └─┘ ┴
214
215 private lemma newton_seq_deriv_norm (n : ℕ) :
id ┴
src ┴
typ ┴
216 ∥F.derivative.eval (newton_seq n)∥ = ∥F.derivative.eval a∥ :=
id ┴┴└─────────┘└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘
217 (newton_seq_aux n).2.1
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ ┴
typ └────────────┘ ┴ ┴ ┴
218
219 private lemma newton_seq_norm_le (n : ℕ) :
id ┴
src ┴
typ ┴
220 ∥F.eval (newton_seq n)∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n) :=
id ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴
src ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴ ┴ ┴ ┴ ┴
typ ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴
doc └───┘ └─────────┘└───┘ ┴
221 (newton_seq_aux n).2.2
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ ┴
typ └────────────┘ ┴ ┴ ┴
222
223 private lemma newton_seq_norm_eq (n : ℕ) :
id ┴
src ┴
typ ┴
224 ∥newton_seq (n+1) - newton_seq n∥ = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ :=
id ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ └────────┘ ┴ ┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ └────────┘ ┴
typ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ └────────┘ ┴ ┴
doc └───┘ └─────────┘└───┘
225 by induction n; simp [newton_seq, newton_seq_aux, ih_n]
id ┴ └────────┘ └────────────┘ └──┘
src └────────┘ └────┘└────────┘└┘└────────────┘└┘└──┘└─
typ └────────┘┴ └────┘└────────┘└┘└────────────┘└┘└──┘└─
doc └────────┘ └────┘ └┘ └┘└──┘└─
txt └────────┘ └────┘ └┘ └┘ └─
par └────────┘ └────┘ └┘ └┘ └─
pid ┴ ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────
226
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
227 private lemma newton_seq_succ_dist (n : ℕ) :
id ┴
src ┴
typ ┴
228 ∥newton_seq (n+1) - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
id ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴
typ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
doc └─────────┘└───┘ ┴
229 calc ∥newton_seq (n+1) - newton_seq n∥
id ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴
typ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴
230 = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ : newton_seq_norm_eq _
id ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ └────────┘ ┴ ┴ └────────────────┘
src ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ └────────┘ ┴ └────────────────┘
typ ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ └────────┘ ┴ ┴ └────────────────┘
doc └───┘ └─────────┘└───┘
231 ... = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval a∥ : by rw newton_seq_deriv_norm
id ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └───────────────────┘
src ┴ └───┘ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ └─┘└───────────────────┘┴
typ ┴┴└───┘ └────────┘ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └─┘└───────────────────┘┴
doc └───┘ └─────────┘└───┘ └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └────────────────────────┘
232 ... ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n) / ∥F.derivative.eval a∥ :
id ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ ┴ └─────────┘└───┘
233 (div_le_div_right deriv_norm_pos).2 (newton_seq_norm_le _)
id └──────────────┘ └────────────┘ ┴ └────────────────┘
src └──────────────┘ └────────────┘ ┴ └────────────────┘
typ └──────────────┘ └────────────┘ ┴ └────────────────┘
234 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel (ne_of_gt deriv_norm_pos) _
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └──────┘ └────────────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ └───────────┘ └──────┘ └────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └───────────┘ └──────┘ └────────────┘
doc └─────────┘└───┘ ┴
235
236 include hnsol
237 private lemma T_pos : T > 0 :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
238 begin
st └─────
239 rw T_def,
id └───┘
src └─┘└───┘
typ └─┘└───┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────┘└─
240 apply div_pos_of_pos_of_pos,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────┘└─
241 { apply (norm_pos_iff _).2,
id └──────────┘
src └────┘ └──────────┘└───┘
typ └────┘ └──────────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └─┘└┘
st ───┘└──────────────────────┘└─
242 apply hnsol },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────┘└┘└
243 { exact deriv_sq_norm_pos hnorm }
id └───────────────┘ └───┘
src └────┘└───────────────┘┴ ┴
typ └────┘└───────────────┘┴└───┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────┘└─
244 end
st ──┘
245
246 private lemma newton_seq_succ_dist_weak (n : ℕ) :
id ┴
src ┴
typ ┴
247 ∥newton_seq (n+2) - newton_seq (n+1)∥ < ∥F.eval a∥ / ∥F.derivative.eval a∥ :=
id ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └───┘ └─────────┘└───┘
248 have 2 ≤ 2^(n+1),
id ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴
249 from have _, from pow_le_pow (by norm_num : 1 ≤ 2) (nat.le_add_left _ _ : 1 ≤ n + 1),
id └────────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └────────┘ └───────┘ ┴ └─────────────┘ ┴ ┴
typ └────────┘ └───────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st └────────┘
250 by simpa using this,
id └──┘
src └──────────┘
typ └──────────┘└──┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └───────────────┘
251 calc ∥newton_seq (n+2) - newton_seq (n+1)∥
id ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴
typ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴
252 ≤ ∥F.derivative.eval a∥ * T^(2^(n+1)) : newton_seq_succ_dist _
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └──────────────────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ ┴ └──────────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └──────────────────┘
doc └─────────┘└───┘ ┴
253 ... ≤ ∥F.derivative.eval a∥ * T^2 : mul_le_mul_of_nonneg_left
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ └───────────────────────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ └───────────────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ └───────────────────────┘
doc └─────────┘└───┘ ┴
254 (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this)
id └──────────────────┘ └─────────┘ └──────┘ └──────┘ └──┘
src └──────────────────┘ └─────────┘ └──────┘ └──────┘
typ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └──┘
255 (norm_nonneg _)
id └─────────┘
src └─────────┘
typ └─────────┘
256 ... < ∥F.derivative.eval a∥ * T^1 : mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_one T_pos T_lt_one (by norm_num))
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ └────────────────────┘ └──────────────────┘ └───┘ └──────┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ └────────────────────┘ └──────────────────┘ └───┘ └──────┘ └──────┘
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ └────────────────────┘ └──────────────────┘ └───┘ └──────┘ └──────┘
doc └─────────┘└───┘ ┴ └──────┘
txt └──────┘
par └──────┘
st └───────┘
257 deriv_norm_pos
id └────────────┘
src └────────────┘
typ └────────────┘
258 ... = ∥F.eval a∥ / ∥F.derivative.eval a∥ :
id ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └───┘ └─────────┘└───┘
259 begin
st └─────
260 rw [T, _root_.pow_two, _root_.pow_one, normed_field.norm_div, ←mul_div_assoc, padic_norm_e.mul],
id ┴ └────────────┘ └────────────┘ └───────────────────┘ └───────────┘ └──────────────┘
src └──┘┴└┘└────────────┘└┘└────────────┘└┘└───────────────────┘└─┘└───────────┘└┘└──────────────┘┴
typ └──┘┴└┘└────────────┘└┘└────────────┘└┘└───────────────────┘└─┘└───────────┘└┘└──────────────┘┴
doc └──┘┴└┘ └┘ └┘ └─┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └─┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └─┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └─┘ └┘ ┴
st ────────┘└──────────────┘└──────────────┘└─────────────────────┘└──────────────┘└────────────────┘└──
261 apply mul_div_mul_left',
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
262 apply deriv_norm_ne_zero; assumption
id └────────────────┘
src └────┘└────────────────┘ └──────────
typ └────┘└────────────────┘ └──────────
doc └────┘ └──────────
txt └────┘ └──────────
par └────┘ └──────────
pid ┴ └
st ─────────────────────────────────────────
263 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
264
265 private lemma newton_seq_dist_aux (n : ℕ) :
id ┴
src ┴
typ ┴
266 ∀ k : ℕ, ∥newton_seq (n + k) - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n)
id ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
src ┴ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴
typ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
doc └─────────┘└───┘ ┴
267 | 0 := begin simp, apply mul_nonneg, {apply norm_nonneg}, {apply T_pow_nonneg} end
id └────────┘ └─────────┘ └──────────┘
src └──┘ └────┘└────────┘ └────┘└─────────┘ └────┘└──────────┘
typ └──┘ └────┘└────────┘ └────┘└─────────┘ └────┘└──────────┘
doc └──┘ └────┘ └────┘ └────┘
txt └──┘ └────┘ └────┘ └────┘
par └──┘ └────┘ └────┘ └────┘
pid ┴ ┴ ┴
st └────────┘└────────────────┘└──────────────────┘└┘└──────────────────┘└───┘
268 | (k+1) :=
id ┴┴
src ┴
typ ┴┴
269 have 2^n ≤ 2^(n+k),
id ┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴┴
270 by {rw [←nat.pow_eq_pow, ←nat.pow_eq_pow], apply pow_le_pow, norm_num, apply nat.le_add_right},
id └────────────┘ └────────────┘ └────────┘ └──────────────┘
src └───┘└────────────┘└─┘└────────────┘┴ └────┘└────────┘ └──────┘ └────┘└──────────────┘
typ └───┘└────────────┘└─┘└────────────┘┴ └────┘└────────┘ └──────┘ └────┘└──────────────┘
doc └───┘ └─┘ ┴ └────┘ └──────┘ └────┘
txt └───┘ └─┘ ┴ └────┘ └──────┘ └────┘
par └───┘ └─┘ ┴ └────┘ └──────┘ └────┘
pid └─┘ └─┘ ┴ ┴ ┴
st └───────────────────┘└───────────────┘└─────────────────┘└────────┘└──────────────────────┘└┘
271 calc
272 ∥newton_seq (n + (k + 1)) - newton_seq n∥
id ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴
src ┴└────────┘ ┴ ┴ ┴ └────────┘ ┴
typ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴
273 = ∥newton_seq ((n + k) + 1) - newton_seq n∥ : by simp
id ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴
src ┴└────────┘ ┴ ┴ ┴ └────────┘ ┴ └───┘
typ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
274 ... = ∥(newton_seq ((n + k) + 1) - newton_seq (n+k)) + (newton_seq (n+k) - newton_seq n)∥ : by rw ←sub_add_sub_cancel
id ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ └────────┘ ┴ ┴ └────────────────┘
src ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ └──┘└────────────────┘┴
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ └────────┘ ┴┴ ┴ └────────┘ ┴ ┴ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └──────────────────────┘
275 ... ≤ max (∥newton_seq ((n + k) + 1) - newton_seq (n+k)∥) (∥newton_seq (n+k) - newton_seq n∥) : padic_norm_z.nonarchimedean _ _
id └─┘ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ └─────────────────────────┘
src └─┘ ┴└────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴└────────┘ ┴ ┴ └────────┘ ┴ └─────────────────────────┘
typ └─┘ ┴└────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴└────────┘ ┴┴ ┴ └────────┘ ┴┴ └─────────────────────────┘
276 ... ≤ max (∥F.derivative.eval a∥ * T^(2^((n + k)))) (∥F.derivative.eval a∥ * T^(2^n)) :
id └─┘ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
src └─┘ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴
typ └─┘ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
doc └─────────┘└───┘ ┴ └─────────┘└───┘ ┴
277 max_le_max (newton_seq_succ_dist _) (newton_seq_dist_aux _)
id └────────┘ └──────────────────┘ └─────────────────┘
src └────────┘ └──────────────────┘
typ └────────┘ └──────────────────┘ └─────────────────┘
278 ... = ∥F.derivative.eval a∥ * T^(2^n) :
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
doc └─────────┘└───┘ ┴
279 max_eq_right $ mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this) (norm_nonneg _)
id └──────────┘ └───────────────────────┘ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └──┘ └─────────┘
src └──────────┘ └───────────────────────┘ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └─────────┘
typ └──────────┘ └───────────────────────┘ └──────────────────┘ └─────────┘ └──────┘ └──────┘ └──┘ └─────────┘
280
281 private lemma newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
282 ∥newton_seq k - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
id ┴└────────┘ ┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
src ┴└────────┘ ┴ └────────┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴
typ ┴└────────┘ ┴ ┴ └────────┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴
doc └─────────┘└───┘ ┴
283 have hex : ∃ m, k = n + m, from exists_eq_add_of_le hnk,
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ └─┘
src ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ └─┘
284 let ⟨_, hex'⟩ := hex in
id └─┘ └─┘
typ └─┘ └─┘
285 by rw hex'; apply newton_seq_dist_aux; assumption
id └──┘ └─────────────────┘
src └─┘ └────┘└─────────────────┘ └──────────
typ └─┘└──┘ └────┘└─────────────────┘ └──────────
doc └─┘ └────┘ └──────────
txt └─┘ └────┘ └──────────
par └─┘ └────┘ └──────────
pid ┴ ┴ └
st └───────────────────────────────────────────────
286
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
287 private lemma newton_seq_dist_to_a : ∀ n : ℕ, 0 < n → ∥newton_seq n - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥
id ┴ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └───┘ └─────────┘└───┘
288 | 1 h := by simp [newton_seq, newton_seq_aux, ih_n]; apply norm_div
id └────────┘ └────────────┘ └──┘
src └────┘└────────┘└┘└────────────┘└┘└──┘┴ └────┘ ┴
typ └────┘└────────┘└┘└────────────┘└┘└──┘┴ └────┘ ┴
doc └────┘ └┘ └┘└──┘┴ └────┘ ┴
txt └────┘ └┘ └┘ ┴ └────┘ ┴
par └────┘ └┘ └┘ ┴ └────┘ ┴
pid ┴┴ └┘ └┘ ┴ ┴ ┴
st └───────────────────────────────────────────────────────┘
289 | (k+2) h :=
id ┴┴
src ┴
typ ┴┴
290 have hlt : ∥newton_seq (k+2) - newton_seq (k+1)∥ < ∥newton_seq (k+1) - a∥,
id ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴
typ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴
291 by rw newton_seq_dist_to_a (k+1) (succ_pos _); apply newton_seq_succ_dist_weak; assumption,
id └──────────────────┘ ┴┴ └──────┘ └───────────────────────┘
src └─┘ ┴ ┴└─┘ └──────┘└─┘ └────┘└───────────────────────┘ └────────┘
typ └─┘└──────────────────┘┴ ┴┴└─┘ └──────┘└─┘ └────┘└───────────────────────┘ └────────┘
doc └─┘ ┴ └─┘ └─┘ └────┘ └────────┘
txt └─┘ ┴ └─┘ └─┘ └────┘ └────────┘
par └─┘ ┴ └─┘ └─┘ └────┘ └────────┘
pid ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────────────────────────────────────────────────────────────┘
292 have hne' : ∥newton_seq (k + 2) - newton_seq (k+1)∥ ≠ ∥newton_seq (k+1) - a∥, from ne_of_lt hlt,
id ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ └──────┘ └─┘
src ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ └──────┘
typ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ └──────┘ └─┘
293 calc ∥newton_seq (k + 2) - a∥
id ┴└────────┘ ┴ ┴ ┴┴
src ┴└────────┘ ┴ ┴ ┴
typ ┴└────────┘ ┴ ┴ ┴┴
294 = ∥(newton_seq (k + 2) - newton_seq (k+1)) + (newton_seq (k+1) - a)∥ : by rw ←sub_add_sub_cancel
id ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────────────┘
src ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └──┘└────────────────┘┴
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └──────────────────────┘
295 ... = max (∥newton_seq (k + 2) - newton_seq (k+1)∥) (∥newton_seq (k+1) - a∥) : padic_norm_z.add_eq_max_of_ne hne'
id └─┘ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ └───────────────────────────┘ └──┘
src └─┘ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ └───────────────────────────┘
typ └─┘ ┴└────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴└────────┘ ┴ ┴ ┴┴ └───────────────────────────┘ └──┘
296 ... = ∥newton_seq (k+1) - a∥ : max_eq_right_of_lt hlt
id ┴└────────┘ ┴ ┴ ┴┴ └────────────────┘ └─┘
src ┴└────────┘ ┴ ┴ ┴ └────────────────┘
typ ┴└────────┘ ┴ ┴ ┴┴ └────────────────┘ └─┘
297 ... = ∥polynomial.eval a F∥ / ∥polynomial.eval a (polynomial.derivative F)∥ : newton_seq_dist_to_a (k+1) (succ_pos _)
id ┴└─────────────┘ ┴ ┴┴ ┴ ┴└─────────────┘ ┴ └───────────────────┘ ┴ ┴ └──────────────────┘ ┴ └──────┘
src ┴└─────────────┘ ┴ ┴ ┴└─────────────┘ └───────────────────┘ ┴ ┴ └──────┘
typ ┴└─────────────┘ ┴ ┴┴ ┴ ┴└─────────────┘ ┴ └───────────────────┘ ┴ ┴ └──────────────────┘ ┴ └──────┘
doc └─────────────┘ └─────────────┘ └───────────────────┘
298
299 private lemma bound' : tendsto (λ n : ℕ, ∥F.derivative.eval a∥ * T^(2^n)) at_top (𝓝 0) :=
id └─────┘ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └────┘ ┴
src └─────┘ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ └────┘ ┴
typ └─────┘ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ └────┘ ┴
doc └─────┘ └─────────┘└───┘ ┴ └────┘ ┴
300 begin
st └─────
301 rw ←mul_zero (∥F.derivative.eval a∥),
id └──────┘ ┴└───────────────┘ ┴┴
src └──┘└──────┘┴ ┴└───────────────┘┴ ┴┴
typ └──┘└──────┘┴ ┴└───────────────┘┴┴┴┴
doc └──┘ ┴ └───────────────┘┴ ┴
txt └──┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
302 exact tendsto_const_nhds.mul
id └────────────────────┘
src └────┘└────────────────────┘└
typ └────┘└────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ───────────────────────────────
303 (tendsto.comp
id └──────────┘
src ───────────────────┘ └──────────┘└
typ ───────────────────┘ └──────────┘└
doc ───────────────────┘ └
txt ───────────────────┘ └
par ───────────────────┘ └
pid ───────────────────┘ └
st ──────────────────────────────────
304 (tendsto_pow_at_top_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm))
id └───────────────────────────────┘ └─────────┘ └──────┘ └───┘
src ─────────────────────┘ └───────────────────────────────┘┴ └─────────┘└──┘ └──────┘┴ └──
typ ─────────────────────┘ └───────────────────────────────┘┴ └─────────┘└──┘ └──────┘┴└───┘└──
doc ─────────────────────┘ ┴ └──┘ ┴ └──
txt ─────────────────────┘ ┴ └──┘ ┴ └──
par ─────────────────────┘ ┴ └──┘ ┴ └──
pid ─────────────────────┘ ┴ └──┘ ┴ └──
st ───────────────────────────────────────────────────────────────────────────────────────────
305 (tendsto_pow_at_top_at_top_of_gt_1_nat (by norm_num)))
id └───────────────────────────────────┘
src ─────────────────────┘ └───────────────────────────────────┘┴ ┴└──────┘└──┘
typ ─────────────────────┘ └───────────────────────────────────┘┴ ┴└──────┘└──┘
doc ─────────────────────┘ ┴ ┴└──────┘└──┘
txt ─────────────────────┘ ┴ ┴└──────┘└──┘
par ─────────────────────┘ ┴ ┴└──────┘└──┘
pid ─────────────────────┘ ┴ └──────────┘┴
st ───────────────────────────────────────────────────────────────┘└───────┘└──┘
306 end
st └─┘
307
308 private lemma bound : ∀ {ε}, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → ∥F.derivative.eval a∥ * T^(2^n) < ε :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └─────────┘└───┘ ┴
309 have mtn : ∀ n : ℕ, ∥polynomial.eval a (polynomial.derivative F)∥ * T ^ (2 ^ n) ≥ 0,
id ┴ ┴└─────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴└─────────────┘ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴└─────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘ └───────────────────┘ ┴
310 from λ n, mul_nonneg (norm_nonneg _) (T_pow_nonneg _),
id ┴ └────────┘ └─────────┘ └──────────┘
src └────────┘ └─────────┘ └──────────┘
typ ┴ └────────┘ └─────────┘ └──────────┘
311 begin
st └─────
312 have := bound' hnorm hnsol,
id └────┘ └───┘ └───┘
src └──────┘└────┘┴ ┴
typ └──────┘└────┘┴└───┘┴└───┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ───────────────────────────┘└─
313 simp [tendsto, nhds] at this,
id └─────┘ └──┘
src └────┘└─────┘└┘└──┘└───────┘
typ └────┘└─────┘└┘└──┘└───────┘
doc └────┘└─────┘└┘└──┘└───────┘
txt └────┘ └┘ └───────┘
par └────┘ └┘ └───────┘
pid ┴┴ └┘ ┴┴└─────┘
st ─────────────────────────────┘└─
314 intros ε hε,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
315 cases this (ball 0 ε) (mem_ball_self hε) (is_open_ball) with N hN,
id └──┘ └──┘ ┴ └───────────┘ └┘ └──────────┘
src └────┘ ┴ └──┘└─┘ └┘ └───────────┘┴ └┘ └──────────┘└─────────┘
typ └────┘└──┘┴ └──┘└─┘┴└┘ └───────────┘┴└┘└┘ └──────────┘└─────────┘
doc └────┘ ┴ └──┘└─┘ └┘ ┴ └┘ └─────────┘
txt └────┘ ┴ └─┘ └┘ ┴ └┘ └─────────┘
par └────┘ ┴ └─┘ └┘ ┴ └┘ └─────────┘
pid ┴ ┴ └─┘ └┘ ┴ └┘ ┴└────────┘
st ──────────────────────────────────────────────────────────────────┘└─
316 existsi N, intros n hn,
id ┴
src └──────┘ └─────────┘
typ └──────┘┴ └─────────┘
doc └──────┘ └─────────┘
txt └──────┘ └─────────┘
par └──────┘ └─────────┘
pid ┴ └───┘
st ──────────┘└───────────┘└─
317 simpa [normed_field.norm_mul, real.norm_eq_abs, abs_of_nonneg (mtn n)] using hN _ hn
id └───────────────────┘ └──────────────┘ └───────────┘ └─┘ ┴ └┘ └┘
src └─────┘└───────────────────┘└┘└──────────────┘└┘└───────────┘┴ ┴ └───────┘ └─┘ ┴
typ └─────┘└───────────────────┘└┘└──────────────┘└┘└───────────┘┴ └─┘┴┴└───────┘└┘└─┘└┘┴
doc └─────┘ └┘ └┘ ┴ ┴ └───────┘ └─┘ ┴
txt └─────┘ └┘ └┘ ┴ ┴ └───────┘ └─┘ ┴
par └─────┘ └┘ └┘ ┴ ┴ └───────┘ └─┘ ┴
pid ┴┴ └┘ └┘ ┴ ┴ └┘┴└────┘ └─┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘
318 end
st └─┘
319
320 private lemma bound'_sq : tendsto (λ n : ℕ, ∥F.derivative.eval a∥^2 * T^(2^n)) at_top (𝓝 0) :=
id └─────┘ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ └────┘ ┴
src └─────┘ ┴ ┴ └─────────┘└───┘ ┴┴ ┴ ┴┴ ┴ └────┘ ┴
typ └─────┘ ┴ ┴┴└─────────┘└───┘ ┴┴┴ ┴ ┴┴ ┴┴ └────┘ ┴
doc └─────┘ └─────────┘└───┘ ┴ └────┘ ┴
321 begin
st └─────
322 rw [←mul_zero (∥F.derivative.eval a∥), _root_.pow_two],
id └──────┘ ┴└───────────────┘ ┴┴ └────────────┘
src └───┘└──────┘┴ ┴└───────────────┘┴ ┴└─┘└────────────┘┴
typ └───┘└──────┘┴ ┴└───────────────┘┴┴┴└─┘└────────────┘┴
doc └───┘ ┴ └───────────────┘┴ └─┘ ┴
txt └───┘ ┴ ┴ └─┘ ┴
par └───┘ ┴ ┴ └─┘ ┴
pid └─┘ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────┘└──────────────┘└──
323 simp only [mul_assoc],
id └───────┘
src └─────────┘└───────┘┴
typ └─────────┘└───────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────┘└─
324 apply tendsto.mul,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
325 { apply tendsto_const_nhds },
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└───────────────────────┘└┘└
326 { apply bound', assumption }
id └────┘
src └────┘└────┘ └─────────┘
typ └────┘└────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ───────────────┘└───────────┘└─
327 end
st ──┘
328
329 private theorem newton_seq_is_cauchy : is_cau_seq norm newton_seq :=
id └────────┘ └──┘ └────────┘
src └────────┘ └──┘ └────────┘
typ └────────┘ └──┘ └────────┘
doc └────────┘
330 begin
st └─────
331 intros ε hε,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
332 cases bound hnorm hnsol hε with N hN,
id └───┘ └───┘ └───┘ └┘
src └────┘└───┘┴ ┴ ┴ └────────┘
typ └────┘└───┘┴└───┘┴└───┘┴└┘└────────┘
doc └────┘ ┴ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ ┴ └────────┘
par └────┘ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ └────────┘
st ─────────────────────────────────────┘└─
333 existsi N,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────┘└─
334 intros j hj,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
335 apply lt_of_le_of_lt,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
336 { apply newton_seq_dist _ _ hj, assumption },
id └─────────────┘ └┘
src └────┘└─────────────┘└───┘ └─────────┘
typ └────┘└─────────────┘└───┘└┘ └─────────┘
doc └────┘ └───┘ └─────────┘
txt └────┘ └───┘ └─────────┘
par └────┘ └───┘ └─────────┘
pid ┴ └───┘ ┴
st ───┘└──────────────────────────┘└───────────┘└┘└
337 { apply hN, apply le_refl }
id └─────┘
src └────┘ └────┘└─────┘┴
typ └────┘ └────┘└─────┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st ───────────┘└──────────────┘└─
338 end
st ──┘
339
340 private def newton_cau_seq : cau_seq ℤ_[p] norm := ⟨_, newton_seq_is_cauchy⟩
id └─────┘ └─┘┴┴ └──┘ └──────────────────┘
src └─────┘ └─┘ ┴ └──┘ └──────────────────┘
typ └─────┘ └─┘┴┴ └──┘ └──────────────────┘
doc └─┘ ┴
341
342 private def soln : ℤ_[p] := newton_cau_seq.lim
id └─┘┴┴ └────────────┘└──┘
src └─┘ ┴ └────────────┘└──┘
typ └─┘┴┴ └────────────┘└──┘
doc └─┘ ┴
343
344 private lemma soln_spec {ε : ℝ} (hε : ε > 0) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
345 ∃ (N : ℕ), ∀ {i : ℕ}, i ≥ N → ∥soln - newton_cau_seq i∥ < ε :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └────────────┘ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └────────────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └────────────┘ ┴┴ ┴ ┴
346 setoid.symm (cau_seq.equiv_lim newton_cau_seq) _ hε
id └─────────┘ └───────────────┘ └────────────┘ └┘
src └─────────┘ └───────────────┘ └────────────┘
typ └─────────┘ └───────────────┘ └────────────┘ └┘
347
348 private lemma soln_deriv_norm : ∥F.derivative.eval soln∥ = ∥F.derivative.eval a∥ :=
id ┴┴└─────────┘└───┘ └──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ └─────────┘└───┘ └──┘┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴└─────────┘└───┘ └──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘ └─────────┘└───┘
349 norm_deriv_eq newton_seq_deriv_norm
id └───────────┘ └───────────────────┘
src └───────────┘ └───────────────────┘
typ └───────────┘ └───────────────────┘
350
351 private lemma newton_seq_norm_tendsto_zero : tendsto (λ i, ∥F.eval (newton_cau_seq i)∥) at_top (𝓝 0) :=
id └─────┘ ┴ ┴┴└───┘ └────────────┘ ┴ ┴ └────┘ ┴
src └─────┘ ┴ └───┘ └────────────┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴┴└───┘ └────────────┘ ┴ ┴ └────┘ ┴
doc └─────┘ └───┘ └────┘ ┴
352 squeeze_zero (λ _, norm_nonneg _) newton_seq_norm_le bound'_sq
id └──────────┘ ┴ └─────────┘ └────────────────┘ └───────┘
src └──────────┘ └─────────┘ └────────────────┘ └───────┘
typ └──────────┘ ┴ └─────────┘ └────────────────┘ └───────┘
353
354 private lemma newton_seq_dist_tendsto :
355 tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (𝓝 (∥F.eval a∥ / ∥F.derivative.eval a∥)) :=
id └─────┘ ┴ ┴└────────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src └─────┘ ┴└────────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ └─────┘ ┴ ┴└────────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────┘ └────┘ ┴ └───┘ └─────────┘└───┘
356 tendsto.congr'
id └────────────┘
src └────────────┘
typ └────────────┘
357 (suffices ∃ k, ∀ n ≥ k, ∥F.eval a∥ / ∥F.derivative.eval a∥ = ∥newton_cau_seq n - a∥, by simpa,
id ┴ ┴┴ ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴└────────────┘ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴└────────────┘ ┴ ┴ └───┘
typ ┴ ┴┴ ┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴└────────────┘ ┴ ┴ ┴┴ └───┘
doc └───┘ └─────────┘└───┘ └───┘
txt └───┘
par └───┘
st └────┘
358 ⟨1, λ _ hx, (newton_seq_dist_to_a _ hx).symm⟩)
id ┴ └┘ └──────────────────┘ └┘ └──┘
src └──────────────────┘ └──┘
typ ┴ └┘ └──────────────────┘ └┘ └──┘
359 (tendsto_const_nhds)
id └────────────────┘
src └────────────────┘
typ └────────────────┘
360
361 private lemma newton_seq_dist_tendsto' :
362 tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (𝓝 ∥soln - a∥) :=
id └─────┘ ┴ ┴└────────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴└──┘ ┴ ┴┴
src └─────┘ ┴└────────────┘ ┴ ┴ └────┘ ┴ ┴└──┘ ┴ ┴
typ └─────┘ ┴ ┴└────────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴└──┘ ┴ ┴┴
doc └─────┘ └────┘ ┴
363 (continuous_norm.tendsto _).comp (newton_cau_seq.tendsto_limit.sub tendsto_const_nhds)
id └─────────────┘└──────┘ └──┘ └────────────┘└────────────┘└──┘ └────────────────┘
src └─────────────┘└──────┘ └──┘ └────────────┘└────────────┘└──┘ └────────────────┘
typ └─────────────┘└──────┘ └──┘ └────────────┘└────────────┘└──┘ └────────────────┘
364
365 private lemma soln_dist_to_a : ∥soln - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥ :=
id ┴└──┘ ┴ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴└──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴└──┘ ┴ ┴┴ ┴ ┴┴└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └───┘ └─────────┘└───┘
366 tendsto_nhds_unique at_top_ne_bot newton_seq_dist_tendsto' newton_seq_dist_tendsto
id └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
src └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
typ └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
367
368 private lemma soln_dist_to_a_lt_deriv : ∥soln - a∥ < ∥F.derivative.eval a∥ :=
id ┴└──┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴└──┘ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴└──┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘
369 begin
st └─────
370 rw soln_dist_to_a,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
371 apply div_lt_of_mul_lt_of_pos,
id └─────────────────────┘
src └────┘└─────────────────────┘
typ └────┘└─────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
372 { apply deriv_norm_pos; assumption },
id └────────────┘
src └────┘└────────────┘ └─────────┘
typ └────┘└────────────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ───┘└───────────────────────────────┘└┘└
373 { rwa _root_.pow_two at hnorm }
id └────────────┘
src └──┘└────────────┘└────────┘
typ └──┘└────────────┘└────────┘
doc └──┘ └────────┘
txt └──┘ └────────┘
par └──┘ └────────┘
pid ┴ └───────┘┴
st ───────────────────────────────┘└─
374 end
st ──┘
375
376 private lemma eval_soln : F.eval soln = 0 :=
id ┴└───┘ └──┘ ┴
src └───┘ └──┘ ┴
typ ┴└───┘ └──┘ ┴
doc └───┘
377 limit_zero_of_norm_tendsto_zero newton_seq_norm_tendsto_zero
id └─────────────────────────────┘ └──────────────────────────┘
src └─────────────────────────────┘ └──────────────────────────┘
typ └─────────────────────────────┘ └──────────────────────────┘
378
379 private lemma soln_unique (z : ℤ_[p]) (hev : F.eval z = 0) (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
id └─┘┴┴ ┴└───┘ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴
typ └─┘┴┴ ┴└───┘ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─┘ ┴ └───┘ └─────────┘└───┘
380 z = soln :=
id ┴ ┴ └──┘
src ┴ └──┘
typ ┴ ┴ └──┘
381 have soln_dist : ∥z - soln∥ < ∥F.derivative.eval a∥, from calc
id ┴┴ ┴ └──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
src ┴ ┴ └──┘┴ ┴ ┴ └─────────┘└───┘ ┴
typ ┴┴ ┴ └──┘┴ ┴ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘
382 ∥z - soln∥ = ∥(z - a) + (a - soln)∥ : by rw sub_add_sub_cancel
id ┴┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────────────────┘
src ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘└────────────────┘└
typ ┴┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘└────────────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └──────────────────────
383 ... ≤ max (∥z - a∥) (∥a - soln∥) : padic_norm_z.nonarchimedean _ _
id └─┘ ┴┴ ┴ ┴┴ ┴┴ ┴ └──┘┴ └─────────────────────────┘
src ───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘┴ └─────────────────────────┘
typ ───────┘ └─┘ ┴┴ ┴ ┴┴ ┴┴ ┴ └──┘┴ └─────────────────────────┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘
384 ... < ∥F.derivative.eval a∥ : max_lt hnlt (by rw norm_sub_rev; apply soln_dist_to_a_lt_deriv),
id ┴┴└─────────┘└───┘ ┴┴ └────┘ └──┘ └──────────┘ └─────────────────────┘
src ┴ └─────────┘└───┘ ┴ └────┘ └─┘└──────────┘ └────┘└─────────────────────┘
typ ┴┴└─────────┘└───┘ ┴┴ └────┘ └──┘ └─┘└──────────┘ └────┘└─────────────────────┘
doc └─────────┘└───┘ └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────────────────────────┘
385 let h := z - soln,
id └─┘ ┴ ┴ ┴ └──┘
src ┴ └──┘
typ └─┘ ┴ ┴ ┴ └──┘
386 ⟨q, hq⟩ := F.binom_expansion soln h in
id ┴ ┴└──────────────┘ └──┘ ┴
src └──────────────┘ └──┘
typ ┴ ┴└──────────────┘ └──┘ ┴
387 have (F.derivative.eval soln + q * h) * h = 0, from eq.symm (calc
id ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └─────┘
typ ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └─────────┘└───┘
388 0 = F.eval (soln + h) : by simp [hev, h]
id ┴└───┘ └──┘ ┴ ┴ └─┘ ┴
src └───┘ └──┘ ┴ └────┘ └┘ └┘
typ ┴└───┘ └──┘ ┴ ┴ └────┘└─┘└┘┴└┘
doc └───┘ └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └─────────────┘
389 ... = F.derivative.eval soln * h + q * h^2 : by rw [hq, eval_soln, zero_add]
id ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴┴ └┘ └───────┘ └──────┘
src └─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └┘└───────┘└┘└──────┘└┘
typ ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴┴ └──┘└┘└┘└───────┘└┘└──────┘└┘
doc └─────────┘└───┘ └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └─────┘└─────────┘└────────┘┴┴
390 ... = (F.derivative.eval soln + q * h) * h : by rw [_root_.pow_two, right_distrib, mul_assoc]),
id ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ └───────────┘ └───────┘
src └─────────┘└───┘ └──┘ ┴ ┴ ┴ └──┘└────────────┘└┘└───────────┘└┘└───────┘┴
typ ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘└────────────┘└┘└───────────┘└┘└───────┘┴
doc └─────────┘└───┘ └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └─────────────────┘└─────────────┘└─────────┘┴
391 have h = 0, from by_contradiction $ λ hne,
id ┴ ┴ └──────────────┘ └─┘
src ┴ └──────────────┘
typ ┴ ┴ └──────────────┘ └─┘
392 have F.derivative.eval soln + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
id ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └───────────────────────────────┘ └──┘ └───────────┘ └─┘
src └─────────┘└───┘ └──┘ ┴ ┴ ┴ └───────────────────────────────┘ └───────────┘
typ ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └───────────────────────────────┘ └──┘ └───────────┘ └─┘
doc └─────────┘└───┘
393 have F.derivative.eval soln = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
id ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └───────────────────┘ └──┘
src └─────────┘└───┘ └──┘ ┴ ┴ ┴ └──────────┘└───────────────────┘┴
typ ┴└─────────┘└───┘ └──┘ ┴ ┴ ┴ ┴ └──────────┘└───────────────────┘┴└──┘
doc └─────────┘└───┘ └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st └─────────────────────────────────────┘
394 lt_irrefl ∥F.derivative.eval soln∥ (calc
id └───────┘ ┴┴└─────────┘└───┘ └──┘┴
src └───────┘ ┴ └─────────┘└───┘ └──┘┴
typ └───────┘ ┴┴└─────────┘└───┘ └──┘┴
doc └─────────┘└───┘
395 ∥F.derivative.eval soln∥ = ∥(-q) * h∥ : by rw this
id ┴┴└─────────┘└───┘ └──┘┴ ┴ ┴ ┴ ┴┴ └──┘
src ┴ └─────────┘└───┘ └──┘┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ ┴┴└─────────┘└───┘ └──┘┴ ┴ ┴ ┴ ┴┴ └─┘└──┘┴
doc └─────────┘└───┘ └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └───────┘
396 ... ≤ 1 * ∥h∥ : by rw [padic_norm_z.mul]; exact mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id ┴ ┴┴┴ └──────────────┘ └────────────────────────┘ └─────────────────┘ └─────────┘
src ┴ ┴ ┴ └──┘└──────────────┘┴ └────┘└────────────────────────┘┴ └─────────────────┘└──┘ └─────────┘└──┘
typ ┴ ┴┴┴ └──┘└──────────────┘┴ └────┘└────────────────────────┘┴ └─────────────────┘└──┘ └─────────┘└──┘
doc └──┘ ┴ └────┘ ┴ └──┘ └──┘
txt └──┘ ┴ └────┘ ┴ └──┘ └──┘
par └──┘ ┴ └────┘ ┴ └──┘ └──┘
pid └┘ ┴ ┴ ┴ └──┘ └─┘┴
st └───────────────────┘┴└─────────────────────────────────────────────────────────────────────────┘
397 ... = ∥z - soln∥ : by simp [h]
id ┴┴ ┴ └──┘┴ ┴
src ┴ ┴ └──┘┴ └────┘ └┘
typ ┴┴ ┴ └──┘┴ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └────────┘
398 ... < ∥F.derivative.eval soln∥ : by rw soln_deriv_norm; apply soln_dist),
id ┴┴└─────────┘└───┘ └──┘┴ └─────────────┘
src ┴ └─────────┘└───┘ └──┘┴ └─┘└─────────────┘ └────┘
typ ┴┴└─────────┘└───┘ └──┘┴ └─┘└─────────────┘ └────┘
doc └─────────┘└───┘ └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────────┘
399 eq_of_sub_eq_zero (by rw ←this; refl)
id └───────────────┘ └──┘
src └───────────────┘ └──┘ └──┘
typ └───────────────┘ └──┘└──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
pid └┘
st └─────────────┘
400
401 end hensel
402
403 variables {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
id ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
src ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
typ ┴ └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
doc └───────┘ └────────┘ └─┘ ┴ └─┘ ┴
404
405 private lemma a_soln_is_unique (ha : F.eval a = 0) (z' : ℤ_[p]) (hz' : F.eval z' = 0)
id ┴└───┘ ┴ ┴ └─┘┴┴ ┴└───┘ └┘ ┴
src └───┘ ┴ └─┘ ┴ └───┘ ┴
typ ┴└───┘ ┴ ┴ └─┘┴┴ ┴└───┘ └┘ ┴
doc └───┘ └─┘ ┴ └───┘
406 (hnormz' : ∥z' - a∥ < ∥F.derivative.eval a∥) : z' = a :=
id ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
doc └─────────┘└───┘
407 let h := z' - a,
id └─┘ ┴ └┘ ┴ ┴
src ┴
typ └─┘ ┴ └┘ ┴ ┴
408 ⟨q, hq⟩ := F.binom_expansion a h in
id ┴ ┴└──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴└──────────────┘ ┴ ┴
409 have (F.derivative.eval a + q * h) * h = 0, from eq.symm (calc
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────────┘└───┘ ┴ ┴ ┴ ┴ └─────┘
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └─────────┘└───┘
410 0 = F.eval (a + h) : show 0 = F.eval (a + (z' - a)), by rw add_comm; simp [hz']
id ┴└───┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └──────┘ └─┘
src └───┘ ┴ ┴ └───┘ ┴ ┴ └─┘└──────┘ └────┘ └┘
typ ┴└───┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └─┘└──────┘ └────┘└─┘└┘
doc └───┘ └───┘ └─┘ └────┘ └┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st └───────────────────────┘
411 ... = F.derivative.eval a * h + q * h^2 : by rw [hq, ha, zero_add]
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └┘ └┘ └──────┘
src └─────────┘└───┘ ┴ ┴ ┴ ┴ └──┘ └┘ └┘└──────┘└┘
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └──┘└┘└┘└┘└┘└──────┘└┘
doc └─────────┘└───┘ └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └─────┘└──┘└────────┘┴┴
412 ... = (F.derivative.eval a + q * h) * h : by rw [_root_.pow_two, right_distrib, mul_assoc]),
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └───────────┘ └───────┘
src └─────────┘└───┘ ┴ ┴ ┴ └──┘└────────────┘└┘└───────────┘└┘└───────┘┴
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└────────────┘└┘└───────────┘└┘└───────┘┴
doc └─────────┘└───┘ └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └─────────────────┘└─────────────┘└─────────┘┴
413 have h = 0, from by_contradiction $ λ hne,
id ┴ ┴ └──────────────┘ └─┘
src ┴ └──────────────┘
typ ┴ ┴ └──────────────┘ └─┘
414 have F.derivative.eval a + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────────────┘ └──┘ └───────────┘ └─┘
src └─────────┘└───┘ ┴ ┴ ┴ └───────────────────────────────┘ └───────────┘
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────────────┘ └──┘ └───────────┘ └─┘
doc └─────────┘└───┘
415 have F.derivative.eval a = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
id ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ └──┘
src └─────────┘└───┘ ┴ ┴ ┴ └──────────┘└───────────────────┘┴
typ ┴└─────────┘└───┘ ┴ ┴ ┴ ┴ ┴ └──────────┘└───────────────────┘┴└──┘
doc └─────────┘└───┘ └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st └─────────────────────────────────────┘
416 lt_irrefl ∥F.derivative.eval a∥ (calc
id └───────┘ ┴┴└─────────┘└───┘ ┴┴
src └───────┘ ┴ └─────────┘└───┘ ┴
typ └───────┘ ┴┴└─────────┘└───┘ ┴┴
doc └─────────┘└───┘
417 ∥F.derivative.eval a∥ = ∥q∥*∥h∥ : by simp [this]
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴┴┴┴ └──┘
src ┴ └─────────┘└───┘ ┴ ┴ ┴┴┴ ┴ └────┘ └─
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴┴┴┴ └────┘└──┘└─
doc └─────────┘└───┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
418 ... ≤ 1*∥h∥ : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id ┴┴┴┴ └────────────────────────┘ └─────────────────┘ └─────────┘
src ───┘ ┴┴ ┴ └────────────────────────┘ └─────────────────┘ └─────────┘
typ ───┘ ┴┴┴┴ └────────────────────────┘ └─────────────────┘ └─────────┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
419 ... < ∥F.derivative.eval a∥ : by simpa [h]),
id ┴┴└─────────┘└───┘ ┴┴ ┴
src ┴ └─────────┘└───┘ ┴ └─────┘ ┴
typ ┴┴└─────────┘└───┘ ┴┴ └─────┘┴┴
doc └─────────┘└───┘ └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └────────┘
420 eq_of_sub_eq_zero (by rw ←this; refl)
id └───────────────┘ └──┘
src └───────────────┘ └──┘ └──┘
typ └───────────────┘ └──┘└──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
pid └┘
st └─────────────┘
421
422 variable (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2)
id ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴
typ ┴ └───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴┴
doc └───┘ └─────────┘└───┘
423 include hnorm
424
425 private lemma a_is_soln (ha : F.eval a = 0) :
id ┴└───┘ ┴ ┴
src └───┘ ┴
typ ┴└───┘ ┴ ┴
doc └───┘
426 F.eval a = 0 ∧ ∥a - a∥ < ∥F.derivative.eval a∥ ∧ ∥F.derivative.eval a∥ = ∥F.derivative.eval a∥ ∧
id ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
doc └───┘ └─────────┘└───┘ └─────────┘└───┘ └─────────┘└───┘
427 ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = a :=
id └┘ ┴└───┘ └┘ ┴ ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ └┘ ┴└───┘ └┘ ┴ ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
doc └───┘ └─────────┘└───┘
428 ⟨ha, by simp; apply deriv_norm_pos; apply hnorm, rfl, a_soln_is_unique ha⟩
id └┘ └────────────┘ └─┘ └──────────────┘ └┘
src └──┘ └────┘└────────────┘ └────┘ └─┘ └──────────────┘
typ └┘ └──┘ └────┘└────────────┘ └────┘ └─┘ └──────────────┘ └┘
doc └──┘ └────┘ └────┘
txt └──┘ └────┘ └────┘
par └──┘ └────┘ └────┘
pid ┴ ┴
st └──────────────────────────────────────┘
429
430 lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥ ∧
id ┴ └─┘┴┴┴ ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
src ┴ └─┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴ └─┘┴┴┴ ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
doc └─┘ ┴ └───┘ └─────────┘└───┘
431 ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧
id ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
src ┴ └─────────┘└───┘ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ ┴┴└─────────┘└───┘ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ ┴
doc └─────────┘└───┘ └─────────┘└───┘
432 ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = z :=
id └┘ ┴└───┘ └┘ ┴ ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴
typ └┘ ┴└───┘ └┘ ┴ ┴└┘ ┴ ┴┴ ┴ ┴┴└─────────┘└───┘ ┴┴ └┘ ┴ ┴
doc └───┘ └─────────┘└───┘
433 if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else
id └┘ ┴└───┘ ┴ ┴ ┴ └───────┘ └───┘ └┘
src └┘ └───┘ ┴ └───────┘
typ └┘ ┴└───┘ ┴ ┴ ┴ └───────┘ └───┘ └┘
doc └───┘
434 by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _, soln_unique _ _⟩;
id └──┘ └───────┘ └─────────────────────┘ └─────────────┘ └─────────┘
src └─────┘ └──┘└────┘└───────┘└────┘└─────────────────────┘└────┘└─────────────┘└────┘└─────────┘└───┘
typ └─────┘ └──┘└────┘└───────┘└────┘└─────────────────────┘└────┘└─────────────┘└────┘└─────────┘└───┘
doc └─────┘ └────┘ └────┘ └────┘ └────┘ └───┘
txt └─────┘ └────┘ └────┘ └────┘ └────┘ └───┘
par └─────┘ └────┘ └────┘ └────┘ └────┘ └───┘
pid ┴ └────┘ └────┘ └────┘ └────┘ └───┘
st └─────────────────────────────────────────────────────────────────────────────────────────────────────
435 assumption
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
st ────────────┘